Encoding 2-player games in QBF correctly and efficiently is challenging and error-prone. To enable concise specifications and uniform encodings of games played on grid boards, like Tic-Tac-Toe, Connect-4, Domineering, Pursuer-Evader and Breakthrough, we introduce BDDL - Board-game Domain Definition Language, inspired by the success of PDDL in the planning domain. We provide an efficient translation from BDDL into QBF, encoding the existence of a winning strategy of bounded depth. Our lifted encoding treats board positions symbolically and allows concise definitions of conditions, effects and winning configurations, relative to symbolic board positions. The size of the encoding grows linearly in the input model and the considered depth. To show the feasibility of such a generic approach, we use QBF solvers to compute the critical depths of winning strategies for instances of several known games. For several games, our work provides the first QBF encoding. Unlike plan validation in SAT-based planning, validating QBF-based winning strategies is difficult. We show how to validate winning strategies using QBF certificates and interactive game play.

We address two bottlenecks for concise QBF encodings of maker-breaker positional games, like Hex and Tic-Tac-Toe. Our baseline is a QBF encoding with explicit variables for board positions and an explicit representation of winning configurations. The first improvement is inspired by lifted planning and avoids variables for explicit board positions, introducing a universal quantifier representing a symbolic board state. The second improvement represents the winning configurations implicitly, exploiting their structure. The paper evaluates the size of several encodings, depending on board size and game depth. It also reports the performance of QBF solvers on these encodings. We evaluate the techniques on Hex instances and also apply them to Harary's Tic-Tac-Toe. In particular, we study scalability to 19$\times$19 boards, played in human Hex tournaments.

Positions of chess players in intransitive (rock-paper-scissors) relations are considered. Namely, position A of White is preferable (it should be chosen if choice is possible) to position B of Black, position B of Black is preferable to position C of White, position C of White is preferable to position D of Black, but position D of Black is preferable to position A of White. Intransitivity of winningness of positions of chess players is considered to be a consequence of complexity of the chess environment -- in contrast with simpler games with transitive positions only. The space of relations between winningness of positions of chess players is non-Euclidean. The Zermelo-von Neumann theorem is complemented by statements about possibility vs. impossibility of building pure winning strategies based on the assumption of transitivity of positions of chess players. Questions about the possibility of intransitive positions of players in other positional games are raised.

Positional games are a mathematical class of two-player games comprising Tictac-toe and its generalizations. We propose a novel encoding of these games into Quantified Boolean Formulas (QBFs) such that a game instance admits a winning strategy for first player if and only if the corresponding formula is true. Our approach improves over previous QBF encodings of games in multiple ways. First, it is generic and lets us encode other positional games, such as Hex. Second, structural properties of positional games together with a careful treatment of illegal moves let us generate more compact instances that can be solved faster by state-of-the-art QBF solvers. We establish the latter fact through extensive experiments. Finally, the compactness of our new encoding makes it feasible to translate realistic game problems. We identify a few such problems of historical significance and put them forward to the QBF community as milestones of increasing difficulty.

We look at the unbiased Maker-Breaker Hamiltonicity game played on the edge set of a complete graph $K_n$, where Maker's goal is to claim a Hamiltonian cycle. First, we prove that, independent of who starts, Maker can win the game for $n = 8$ and $n = 9$. Then we use an inductive argument to show that, independent of who starts, Maker can win the game if and only if $n \geq 8$. This, in particular, resolves in the affirmative the long-standing conjecture of Papaioannou. We also study two standard positional games related to Hamiltonicity game. For Hamiltonian Path game, we show that Maker can claim a Hamiltonian path if and only if $n \geq 5$, independent of who starts. Next, we look at Fixed Hamiltonian Path game, where the goal of Maker is to claim a Hamiltonian path between two predetermined vertices. We prove that if Maker starts the game, he wins if and only if $n \geq 7$, and if Breaker starts, Maker wins if and only if $n \geq 8$. Using this result, we are able to improve the previously best upper bound on the smallest number of edges a graph on $n$ vertices can have, knowing that Maker can win the Maker-Breaker Hamiltonicity game played on its edges. To resolve the outcomes of the mentioned games on small (finite) boards, we devise algorithms for efficiently searching game trees and then obtain our results with the help of a computer.